#include "itp.h"
#include "Sort.h"
using namespace MinisatProof;

const AigLit ITP::VarA;
const AigLit ITP::VarB;

std::ostream & operator<<( std::ostream & out , const Lit & l )
{
   out << (sign(l)?'-':' ') << var(l) ;
   return out;
}

/// if A return 0 if B return 1 
void PITP::root( const vec<Lit> & c , uint8_t x)
{
   _subITP.push( _camp[x]?0:1 );
}
inline bool isGlobal( AigLit v ){ return (v&0x8000000)==0;}
/// sequence of resolution ( backtrace to fist UIP )
void PITP::chain( const vec<ClauseId> & cs , const vec<Lit> & xs )
{
   AigLit p = _subITP[ cs[0] ];
   for( int i = 0 ; i < xs.size() ; ++ i )
      p = resolve(p , xs[i] , _subITP[ cs[i+1] ] );
   _subITP.push( p );
}  

//inline bool isGlobal( AigLit v ){ return (v&0x8000000)==0;}
/// if pivot (a)  OR , (b)  AND, (global) ITE
AigLit PITP::resolve(AigLit p , Lit l , AigLit q)
{
    Var v = var(l);

    if( isGlobal( _base[v] ) ) //Global
       return ITE( _base[v]^sign(l) , q , p );
    else if( _base[v] == ITP::VarA )
        return  OR( p , q) ;
    else 
        return  AND( p , q );
}
void SPITP::done( unsigned id , const vec<Lit> & c )
{
    AigLit p =  _subITP[ id ];
    
    for( int i = 0 ; i < c.size() ; ++ i )
       if( isGlobal( _base[ var(c[i])] ) )
          p = AND( p ,  _base[ var(c[i]) ]^sign(c[i])^1 );

    _interpolant = p;
}


/// if A conjuction of Global , B const 1 
void MITP::root( const vec<Lit> & c , uint8_t x)
{
    //cout << _subITP.size() << " : ";
    //for( unsigned i = 0 ; i < c.size() ; ++ i )
    //   cout << c[i] << " "; cout << endl;

    AigLit p ;

    if( _camp[x] !=_inv)
    {
       p = toAigLit( 0 , 0 );
       for( int i = 0 ; i < c.size() ; ++i)
       {
          Var v = var( c[i] );
          if( isGlobal( _base[v] ) )//Global
            p = OR( p , _base[v]^sign(c[i]) );
       }
    }else
       p = toAigLit( 0 , 1 );

    _subITP.push( p );
}
void MITP::chain( const vec<ClauseId> & cs , const vec<Lit> & xs )
{
   //cout << _subITP.size() << " : ";
   //for( unsigned i = 0 ; i  < cs.size() ; ++ i )
   //   cout << cs[i] << " " ; cout << endl;

   AigLit p = _subITP[ cs[0] ];
   for( int i = 0 ; i < xs.size() ; ++ i )
      p = resolve(p , xs[i] , _subITP[ cs[i+1] ] );

   _subITP.push( p );
}
AigLit MITP::resolve(AigLit p , Lit l , AigLit q)
{
    if( _base[var(l)] == (_inv?ITP::VarB:ITP::VarA) )
        return  OR( p,q );
    else 
        return AND( p,q );
}
void SMITP::done( unsigned id , const vec<Lit> & c )
{
    //AigLit p = _inv?(inv(_subITP.last())):_subITP.last();
    AigLit p = _inv ? inv( _subITP[ id ] ) : _subITP[ id ];
    
   
    for( int i = 0 ; i < c.size() ; ++ i )
       if( isGlobal( _base[ var(c[i])] ) )
          p = AND( p ,  _base[ var(c[i]) ]^sign(c[i])^1 );

    _interpolant = p;
}


MultiSITP::MultiSITP(unsigned n ) : _sitp( n , NULL ){}
MultiSITP::~MultiSITP()
{
   for( unsigned i = 0 ; i < _sitp.size() ; ++i )delete _sitp[i] ;
}
void MultiSITP::root   (const vec<Lit>& c , uint8_t A)
{   
    for( unsigned i = 0 ; i < _sitp.size() ; ++i )_sitp[i]->root(c,A);
}
void MultiSITP::chain  (const vec<ClauseId>& cs, const vec<Lit>& xs)
{
    for( unsigned i = 0 ; i < _sitp.size() ; ++i )_sitp[i]->chain(cs,xs);
}
void MultiSITP::deleted(ClauseId c)
{
    for( unsigned i = 0 ; i < _sitp.size() ; ++i )_sitp[i]->deleted(c);
}
void MultiSITP::done   ()
{
    for( unsigned i = 0 ; i < _sitp.size() ; ++i )_sitp[i]->done();
}
//=============================================================================


ProofTraverser * ITPMgr::init( Solver & S ,  StrashAIG & ckt) 
{
   if( MODE == NONE )return NULL;
   S.expensive_ccmin = CC_MIN ; 
   
   switch( ITP )
   {
		case  PUDLARK : _itp = new SPITP( ckt ); break;
		case  MCMILLIAN : _itp = new SMITP( ckt , ITP_PHASE ); break;
		default:exit(0);break;
   }
   
   switch( MODE )
   {
      case ON_THE_FLY : _pft = _itp ; break;
      case HDD        : _pft = NULL ; break; /// refine 
      case MEM        : _pft = new Checker( false ); break;// false only record
	  default:exit(0);break;
   }

   if( _pft ) _pf = S.proof = new Proof( * _pft ) ;/// check TODO
   else       _pf = S.proof = new Proof();
   return _pft;
}
AigLit ITPMgr::itpGen()
{
	assert( MODE != NONE );
    if( MODE != ON_THE_FLY )
    {
       if( MODE == MEM )
          dynamic_cast<Checker *>(_pft)->traverse( *_itp ); 
       else if( MODE == HDD )
          _pf->traverse( *_itp);
    }
	_itp->done();//TODO
	_interpolant = _itp->interpolant();
    return _interpolant;
}

ITPMgr::~ITPMgr()
{
   if( MODE == NONE ) return;
   delete    _pf;
   delete    _itp;
   if( MODE != ON_THE_FLY ) delete _pft;
}

//=== console text proof construction ========================================
void Checker::root   (const vec<Lit>& c , uint8_t A) 
{
    vcs.push();
    vxs.push();
    phase.push( A );

    clauses.push();
    c.copyTo(clauses.last()); 
}
void Checker::chain  (const vec<ClauseId>& cs, const vec<Lit>& xs) 
{
    vcs.push();
    vxs.push();
    cs.copyTo( vcs.last());
    xs.copyTo( vxs.last());

    clauses.push();
    phase.push( 0xFF ); // 0xFF means chain 

    if( _resolve_check )
    {
       vec<Lit> p;
       clauses[ cs[0] ].copyTo( p );
       for( int i = 0 ; i < xs.size() ; ++ i )
         resolve( p , xs[i] , clauses[ cs[i+1] ] );
       p.copyTo( clauses.last() );
    }
}

void Checker::deleted(ClauseId c) 
{
}
void Checker::done()
{

}
void Checker::resolve(vec<Lit>& main, Lit l ,  vec<Lit>& other)
{
   unsigned checkcnt = 0 ;
   int j = 0;
   for( int i = 0 ; i < main.size() ; ++i ) 
      if( var( main[i] ) != var( l ) )
         main[ j++ ] = main[i]; 
      else
      {
         assert( sign( main[i] ) == sign( l ) );
         checkcnt+=1;
      }
   main.shrink( checkcnt );
   for( int i = 0 ; i < other.size() ; ++i )
      if( var( other[i] ) != var(l) )
         main.push( other[i] );
      else 
      {
         assert( sign( other[i] ) != sign( l ) );
         checkcnt+=1;
      }
   assert( checkcnt >= 2 );
}
void Checker::traverse( ProofTraverser & itp )
{
   for( int i = TRA_INT ; i < clauses.size() ; ++i )
      if( phase[i] != 0xFF )
         itp.root( clauses[i] , phase[i] );
      else 
         itp.chain( vcs[i] , vxs[i] );
   TRA_INT = clauses.size();
}
//=============================================================================

